terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
SQR1(s1(X)) -> ADD2(sqr1(X), dbl1(X))
ADD2(s1(X), Y) -> ADD2(X, Y)
SQR1(s1(X)) -> SQR1(X)
SQR1(s1(X)) -> DBL1(X)
TERMS1(N) -> SQR1(N)
ACTIVATE1(n__first2(X1, X2)) -> FIRST2(X1, X2)
FIRST2(s1(X), cons2(Y, Z)) -> ACTIVATE1(Z)
DBL1(s1(X)) -> DBL1(X)
ACTIVATE1(n__terms1(X)) -> TERMS1(X)
HALF1(s1(s1(X))) -> HALF1(X)
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
SQR1(s1(X)) -> ADD2(sqr1(X), dbl1(X))
ADD2(s1(X), Y) -> ADD2(X, Y)
SQR1(s1(X)) -> SQR1(X)
SQR1(s1(X)) -> DBL1(X)
TERMS1(N) -> SQR1(N)
ACTIVATE1(n__first2(X1, X2)) -> FIRST2(X1, X2)
FIRST2(s1(X), cons2(Y, Z)) -> ACTIVATE1(Z)
DBL1(s1(X)) -> DBL1(X)
ACTIVATE1(n__terms1(X)) -> TERMS1(X)
HALF1(s1(s1(X))) -> HALF1(X)
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
HALF1(s1(s1(X))) -> HALF1(X)
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
HALF1(s1(s1(X))) -> HALF1(X)
[HALF1, s1]
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
ADD2(s1(X), Y) -> ADD2(X, Y)
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
ADD2(s1(X), Y) -> ADD2(X, Y)
[ADD1, s1]
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
DBL1(s1(X)) -> DBL1(X)
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
DBL1(s1(X)) -> DBL1(X)
s1 > DBL1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
SQR1(s1(X)) -> SQR1(X)
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
SQR1(s1(X)) -> SQR1(X)
s1 > SQR1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
ACTIVATE1(n__first2(X1, X2)) -> FIRST2(X1, X2)
FIRST2(s1(X), cons2(Y, Z)) -> ACTIVATE1(Z)
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X
The following pairs can be strictly oriented and are deleted.
The remaining pairs can at least by weakly be oriented.
ACTIVATE1(n__first2(X1, X2)) -> FIRST2(X1, X2)
Used ordering: Combined order from the following AFS and order.
FIRST2(s1(X), cons2(Y, Z)) -> ACTIVATE1(Z)
s > [ACTIVATE1, nfirst2, FIRST1]
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
FIRST2(s1(X), cons2(Y, Z)) -> ACTIVATE1(Z)
terms1(N) -> cons2(recip1(sqr1(N)), n__terms1(s1(N)))
sqr1(0) -> 0
sqr1(s1(X)) -> s1(add2(sqr1(X), dbl1(X)))
dbl1(0) -> 0
dbl1(s1(X)) -> s1(s1(dbl1(X)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
first2(0, X) -> nil
first2(s1(X), cons2(Y, Z)) -> cons2(Y, n__first2(X, activate1(Z)))
half1(0) -> 0
half1(s1(0)) -> 0
half1(s1(s1(X))) -> s1(half1(X))
half1(dbl1(X)) -> X
terms1(X) -> n__terms1(X)
first2(X1, X2) -> n__first2(X1, X2)
activate1(n__terms1(X)) -> terms1(X)
activate1(n__first2(X1, X2)) -> first2(X1, X2)
activate1(X) -> X